$\forall$${\it es}$:ES, $e$, $a$:E. $a$ $\leq$loc $e$  $\Rightarrow$ (es{-}le{-}before(${\it es}$;$e$) = (before($a$) @ [$a$, $e$]) $\in$ (E List))